A:Type, X:MaInterface(A), es:ES. ma-interface-consistent(es;X)  ([[X]]  AbsInterface(A)) 

latex

Definitions

AbsInterface(A), [[X]], if b then t else f fi , ma-in-interface(es;X;e), , x:A.B(x), Void, x.A(x), P  Q, , s = t, b, ma-interface-val(es;X;e), A, False, E, t.1, ma-interface-consistent(es;X), ma-interface-consistent-at(es;i;X), MaInterface(T), a:A fp B(a), let x,y = A in B(x;y), Top, P & Q, constant_function(f;A;B), b, , x:A. B(x), P  Q, r  s, e < e', val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), , , type List, Msg(M), kindcase(k; a.f(a); l,t.g(l;t) ), Knd, EState(T), f(a), EOrderAxioms(E; pred?; info), Id, x:A  B(x), IdLnk, x:AB(x), left + right, Unit, EqDecider(T), Type, ES, ff, t  T, inr x

Lemmas

bfalse wf, ma-interface-val wf, bool wf, assert wf, not wf, bnot wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, es-E wf, it wf, top wf, ma-in-interface wf, ifthenelse wf, ma-interface wf, event system wf, ma-interface-consistent wf